x, y:Atom. (x =a y = tt  )  (x = y) 

latex

Up	sqequal 1, sqequal 1
Definitions	, t  T, P  Q, x:A. B(x), P & Q, P  Q
Lemmas	btrue wf, eq atom wf, bool wf, assert of eq atom, eqtt to assert, assert wf, iff transitivity